0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 285 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 262 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 PiDPToQDPProof (⇒, 0 ms)
↳16 QDP
↳17 Rewriting (⇔, 0 ms)
↳18 QDP
↳19 UsableRulesProof (⇔, 0 ms)
↳20 QDP
↳21 QReductionProof (⇔, 0 ms)
↳22 QDP
↳23 QDPOrderProof (⇔, 26 ms)
↳24 QDP
↳25 DependencyGraphProof (⇔, 0 ms)
↳26 TRUE
LOG2D_IN_GA(s(s(X1)), X2) → U6_GA(X1, X2, halfB_in_ga(X1, X3))
LOG2D_IN_GA(s(s(X1)), X2) → HALFB_IN_GA(X1, X3)
HALFB_IN_GA(X1, s(X2)) → U2_GA(X1, X2, halfA_in_ga(X1, X2))
HALFB_IN_GA(X1, s(X2)) → HALFA_IN_GA(X1, X2)
HALFA_IN_GA(s(s(X1)), s(X2)) → U1_GA(X1, X2, halfA_in_ga(X1, X2))
HALFA_IN_GA(s(s(X1)), s(X2)) → HALFA_IN_GA(X1, X2)
LOG2D_IN_GA(s(s(X1)), X2) → U7_GA(X1, X2, halfcB_in_ga(X1, s(s(X3))))
U7_GA(X1, X2, halfcB_out_ga(X1, s(s(X3)))) → U8_GA(X1, X2, halfB_in_ga(X3, X4))
U7_GA(X1, X2, halfcB_out_ga(X1, s(s(X3)))) → HALFB_IN_GA(X3, X4)
U7_GA(X1, X2, halfcB_out_ga(X1, s(s(X3)))) → U9_GA(X1, X2, halfcB_in_ga(X3, s(s(X4))))
U9_GA(X1, X2, halfcB_out_ga(X3, s(s(X4)))) → U10_GA(X1, X2, halfB_in_ga(X4, X5))
U9_GA(X1, X2, halfcB_out_ga(X3, s(s(X4)))) → HALFB_IN_GA(X4, X5)
U9_GA(X1, X2, halfcB_out_ga(X3, s(s(X4)))) → U11_GA(X1, X2, halfcB_in_ga(X4, s(s(X5))))
U11_GA(X1, X2, halfcB_out_ga(X4, s(s(X5)))) → U12_GA(X1, X2, halfB_in_ga(X5, X6))
U11_GA(X1, X2, halfcB_out_ga(X4, s(s(X5)))) → HALFB_IN_GA(X5, X6)
U11_GA(X1, X2, halfcB_out_ga(X4, s(s(X5)))) → U13_GA(X1, X2, halfcB_in_ga(X5, s(s(X6))))
U13_GA(X1, X2, halfcB_out_ga(X5, s(s(X6)))) → U14_GA(X1, X2, halfB_in_ga(X6, X7))
U13_GA(X1, X2, halfcB_out_ga(X5, s(s(X6)))) → HALFB_IN_GA(X6, X7)
U13_GA(X1, X2, halfcB_out_ga(X5, s(s(X6)))) → U15_GA(X1, X2, halfcB_in_ga(X6, s(s(X7))))
U15_GA(X1, X2, halfcB_out_ga(X6, s(s(X7)))) → U16_GA(X1, X2, halfB_in_ga(X7, X8))
U15_GA(X1, X2, halfcB_out_ga(X6, s(s(X7)))) → HALFB_IN_GA(X7, X8)
U15_GA(X1, X2, halfcB_out_ga(X6, s(s(X7)))) → U17_GA(X1, X2, halfcB_in_ga(X7, s(s(X8))))
U17_GA(X1, X2, halfcB_out_ga(X7, s(s(X8)))) → U18_GA(X1, X2, halfB_in_ga(X8, X9))
U17_GA(X1, X2, halfcB_out_ga(X7, s(s(X8)))) → HALFB_IN_GA(X8, X9)
U17_GA(X1, X2, halfcB_out_ga(X7, s(s(X8)))) → U19_GA(X1, X2, halfcB_in_ga(X8, s(s(X9))))
U19_GA(X1, X2, halfcB_out_ga(X8, s(s(X9)))) → U20_GA(X1, X2, pC_in_gaga(X9, X10, s(s(s(s(s(s(s(0))))))), X2))
U19_GA(X1, X2, halfcB_out_ga(X8, s(s(X9)))) → PC_IN_GAGA(X9, X10, s(s(s(s(s(s(s(0))))))), X2)
PC_IN_GAGA(X1, X2, X3, X4) → U3_GAGA(X1, X2, X3, X4, halfB_in_ga(X1, X2))
PC_IN_GAGA(X1, X2, X3, X4) → HALFB_IN_GA(X1, X2)
PC_IN_GAGA(X1, s(s(X2)), X3, X4) → U4_GAGA(X1, X2, X3, X4, halfcB_in_ga(X1, s(s(X2))))
U4_GAGA(X1, X2, X3, X4, halfcB_out_ga(X1, s(s(X2)))) → U5_GAGA(X1, X2, X3, X4, pC_in_gaga(X2, X5, s(X3), X4))
U4_GAGA(X1, X2, X3, X4, halfcB_out_ga(X1, s(s(X2)))) → PC_IN_GAGA(X2, X5, s(X3), X4)
halfcB_in_ga(X1, s(X2)) → U23_ga(X1, X2, halfcA_in_ga(X1, X2))
halfcA_in_ga(0, 0) → halfcA_out_ga(0, 0)
halfcA_in_ga(s(0), 0) → halfcA_out_ga(s(0), 0)
halfcA_in_ga(s(s(X1)), s(X2)) → U22_ga(X1, X2, halfcA_in_ga(X1, X2))
U22_ga(X1, X2, halfcA_out_ga(X1, X2)) → halfcA_out_ga(s(s(X1)), s(X2))
U23_ga(X1, X2, halfcA_out_ga(X1, X2)) → halfcB_out_ga(X1, s(X2))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
LOG2D_IN_GA(s(s(X1)), X2) → U6_GA(X1, X2, halfB_in_ga(X1, X3))
LOG2D_IN_GA(s(s(X1)), X2) → HALFB_IN_GA(X1, X3)
HALFB_IN_GA(X1, s(X2)) → U2_GA(X1, X2, halfA_in_ga(X1, X2))
HALFB_IN_GA(X1, s(X2)) → HALFA_IN_GA(X1, X2)
HALFA_IN_GA(s(s(X1)), s(X2)) → U1_GA(X1, X2, halfA_in_ga(X1, X2))
HALFA_IN_GA(s(s(X1)), s(X2)) → HALFA_IN_GA(X1, X2)
LOG2D_IN_GA(s(s(X1)), X2) → U7_GA(X1, X2, halfcB_in_ga(X1, s(s(X3))))
U7_GA(X1, X2, halfcB_out_ga(X1, s(s(X3)))) → U8_GA(X1, X2, halfB_in_ga(X3, X4))
U7_GA(X1, X2, halfcB_out_ga(X1, s(s(X3)))) → HALFB_IN_GA(X3, X4)
U7_GA(X1, X2, halfcB_out_ga(X1, s(s(X3)))) → U9_GA(X1, X2, halfcB_in_ga(X3, s(s(X4))))
U9_GA(X1, X2, halfcB_out_ga(X3, s(s(X4)))) → U10_GA(X1, X2, halfB_in_ga(X4, X5))
U9_GA(X1, X2, halfcB_out_ga(X3, s(s(X4)))) → HALFB_IN_GA(X4, X5)
U9_GA(X1, X2, halfcB_out_ga(X3, s(s(X4)))) → U11_GA(X1, X2, halfcB_in_ga(X4, s(s(X5))))
U11_GA(X1, X2, halfcB_out_ga(X4, s(s(X5)))) → U12_GA(X1, X2, halfB_in_ga(X5, X6))
U11_GA(X1, X2, halfcB_out_ga(X4, s(s(X5)))) → HALFB_IN_GA(X5, X6)
U11_GA(X1, X2, halfcB_out_ga(X4, s(s(X5)))) → U13_GA(X1, X2, halfcB_in_ga(X5, s(s(X6))))
U13_GA(X1, X2, halfcB_out_ga(X5, s(s(X6)))) → U14_GA(X1, X2, halfB_in_ga(X6, X7))
U13_GA(X1, X2, halfcB_out_ga(X5, s(s(X6)))) → HALFB_IN_GA(X6, X7)
U13_GA(X1, X2, halfcB_out_ga(X5, s(s(X6)))) → U15_GA(X1, X2, halfcB_in_ga(X6, s(s(X7))))
U15_GA(X1, X2, halfcB_out_ga(X6, s(s(X7)))) → U16_GA(X1, X2, halfB_in_ga(X7, X8))
U15_GA(X1, X2, halfcB_out_ga(X6, s(s(X7)))) → HALFB_IN_GA(X7, X8)
U15_GA(X1, X2, halfcB_out_ga(X6, s(s(X7)))) → U17_GA(X1, X2, halfcB_in_ga(X7, s(s(X8))))
U17_GA(X1, X2, halfcB_out_ga(X7, s(s(X8)))) → U18_GA(X1, X2, halfB_in_ga(X8, X9))
U17_GA(X1, X2, halfcB_out_ga(X7, s(s(X8)))) → HALFB_IN_GA(X8, X9)
U17_GA(X1, X2, halfcB_out_ga(X7, s(s(X8)))) → U19_GA(X1, X2, halfcB_in_ga(X8, s(s(X9))))
U19_GA(X1, X2, halfcB_out_ga(X8, s(s(X9)))) → U20_GA(X1, X2, pC_in_gaga(X9, X10, s(s(s(s(s(s(s(0))))))), X2))
U19_GA(X1, X2, halfcB_out_ga(X8, s(s(X9)))) → PC_IN_GAGA(X9, X10, s(s(s(s(s(s(s(0))))))), X2)
PC_IN_GAGA(X1, X2, X3, X4) → U3_GAGA(X1, X2, X3, X4, halfB_in_ga(X1, X2))
PC_IN_GAGA(X1, X2, X3, X4) → HALFB_IN_GA(X1, X2)
PC_IN_GAGA(X1, s(s(X2)), X3, X4) → U4_GAGA(X1, X2, X3, X4, halfcB_in_ga(X1, s(s(X2))))
U4_GAGA(X1, X2, X3, X4, halfcB_out_ga(X1, s(s(X2)))) → U5_GAGA(X1, X2, X3, X4, pC_in_gaga(X2, X5, s(X3), X4))
U4_GAGA(X1, X2, X3, X4, halfcB_out_ga(X1, s(s(X2)))) → PC_IN_GAGA(X2, X5, s(X3), X4)
halfcB_in_ga(X1, s(X2)) → U23_ga(X1, X2, halfcA_in_ga(X1, X2))
halfcA_in_ga(0, 0) → halfcA_out_ga(0, 0)
halfcA_in_ga(s(0), 0) → halfcA_out_ga(s(0), 0)
halfcA_in_ga(s(s(X1)), s(X2)) → U22_ga(X1, X2, halfcA_in_ga(X1, X2))
U22_ga(X1, X2, halfcA_out_ga(X1, X2)) → halfcA_out_ga(s(s(X1)), s(X2))
U23_ga(X1, X2, halfcA_out_ga(X1, X2)) → halfcB_out_ga(X1, s(X2))
HALFA_IN_GA(s(s(X1)), s(X2)) → HALFA_IN_GA(X1, X2)
halfcB_in_ga(X1, s(X2)) → U23_ga(X1, X2, halfcA_in_ga(X1, X2))
halfcA_in_ga(0, 0) → halfcA_out_ga(0, 0)
halfcA_in_ga(s(0), 0) → halfcA_out_ga(s(0), 0)
halfcA_in_ga(s(s(X1)), s(X2)) → U22_ga(X1, X2, halfcA_in_ga(X1, X2))
U22_ga(X1, X2, halfcA_out_ga(X1, X2)) → halfcA_out_ga(s(s(X1)), s(X2))
U23_ga(X1, X2, halfcA_out_ga(X1, X2)) → halfcB_out_ga(X1, s(X2))
HALFA_IN_GA(s(s(X1)), s(X2)) → HALFA_IN_GA(X1, X2)
HALFA_IN_GA(s(s(X1))) → HALFA_IN_GA(X1)
From the DPs we obtained the following set of size-change graphs:
PC_IN_GAGA(X1, s(s(X2)), X3, X4) → U4_GAGA(X1, X2, X3, X4, halfcB_in_ga(X1, s(s(X2))))
U4_GAGA(X1, X2, X3, X4, halfcB_out_ga(X1, s(s(X2)))) → PC_IN_GAGA(X2, X5, s(X3), X4)
halfcB_in_ga(X1, s(X2)) → U23_ga(X1, X2, halfcA_in_ga(X1, X2))
halfcA_in_ga(0, 0) → halfcA_out_ga(0, 0)
halfcA_in_ga(s(0), 0) → halfcA_out_ga(s(0), 0)
halfcA_in_ga(s(s(X1)), s(X2)) → U22_ga(X1, X2, halfcA_in_ga(X1, X2))
U22_ga(X1, X2, halfcA_out_ga(X1, X2)) → halfcA_out_ga(s(s(X1)), s(X2))
U23_ga(X1, X2, halfcA_out_ga(X1, X2)) → halfcB_out_ga(X1, s(X2))
PC_IN_GAGA(X1, X3) → U4_GAGA(X1, X3, halfcB_in_ga(X1))
U4_GAGA(X1, X3, halfcB_out_ga(X1, s(s(X2)))) → PC_IN_GAGA(X2, s(X3))
halfcB_in_ga(X1) → U23_ga(X1, halfcA_in_ga(X1))
halfcA_in_ga(0) → halfcA_out_ga(0, 0)
halfcA_in_ga(s(0)) → halfcA_out_ga(s(0), 0)
halfcA_in_ga(s(s(X1))) → U22_ga(X1, halfcA_in_ga(X1))
U22_ga(X1, halfcA_out_ga(X1, X2)) → halfcA_out_ga(s(s(X1)), s(X2))
U23_ga(X1, halfcA_out_ga(X1, X2)) → halfcB_out_ga(X1, s(X2))
halfcB_in_ga(x0)
halfcA_in_ga(x0)
U22_ga(x0, x1)
U23_ga(x0, x1)
PC_IN_GAGA(X1, X3) → U4_GAGA(X1, X3, U23_ga(X1, halfcA_in_ga(X1)))
U4_GAGA(X1, X3, halfcB_out_ga(X1, s(s(X2)))) → PC_IN_GAGA(X2, s(X3))
PC_IN_GAGA(X1, X3) → U4_GAGA(X1, X3, U23_ga(X1, halfcA_in_ga(X1)))
halfcB_in_ga(X1) → U23_ga(X1, halfcA_in_ga(X1))
halfcA_in_ga(0) → halfcA_out_ga(0, 0)
halfcA_in_ga(s(0)) → halfcA_out_ga(s(0), 0)
halfcA_in_ga(s(s(X1))) → U22_ga(X1, halfcA_in_ga(X1))
U22_ga(X1, halfcA_out_ga(X1, X2)) → halfcA_out_ga(s(s(X1)), s(X2))
U23_ga(X1, halfcA_out_ga(X1, X2)) → halfcB_out_ga(X1, s(X2))
halfcB_in_ga(x0)
halfcA_in_ga(x0)
U22_ga(x0, x1)
U23_ga(x0, x1)
U4_GAGA(X1, X3, halfcB_out_ga(X1, s(s(X2)))) → PC_IN_GAGA(X2, s(X3))
PC_IN_GAGA(X1, X3) → U4_GAGA(X1, X3, U23_ga(X1, halfcA_in_ga(X1)))
halfcA_in_ga(0) → halfcA_out_ga(0, 0)
halfcA_in_ga(s(0)) → halfcA_out_ga(s(0), 0)
halfcA_in_ga(s(s(X1))) → U22_ga(X1, halfcA_in_ga(X1))
U23_ga(X1, halfcA_out_ga(X1, X2)) → halfcB_out_ga(X1, s(X2))
U22_ga(X1, halfcA_out_ga(X1, X2)) → halfcA_out_ga(s(s(X1)), s(X2))
halfcB_in_ga(x0)
halfcA_in_ga(x0)
U22_ga(x0, x1)
U23_ga(x0, x1)
halfcB_in_ga(x0)
U4_GAGA(X1, X3, halfcB_out_ga(X1, s(s(X2)))) → PC_IN_GAGA(X2, s(X3))
PC_IN_GAGA(X1, X3) → U4_GAGA(X1, X3, U23_ga(X1, halfcA_in_ga(X1)))
halfcA_in_ga(0) → halfcA_out_ga(0, 0)
halfcA_in_ga(s(0)) → halfcA_out_ga(s(0), 0)
halfcA_in_ga(s(s(X1))) → U22_ga(X1, halfcA_in_ga(X1))
U23_ga(X1, halfcA_out_ga(X1, X2)) → halfcB_out_ga(X1, s(X2))
U22_ga(X1, halfcA_out_ga(X1, X2)) → halfcA_out_ga(s(s(X1)), s(X2))
halfcA_in_ga(x0)
U22_ga(x0, x1)
U23_ga(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U4_GAGA(X1, X3, halfcB_out_ga(X1, s(s(X2)))) → PC_IN_GAGA(X2, s(X3))
POL(0) = 0
POL(PC_IN_GAGA(x1, x2)) = 1 + x1
POL(U22_ga(x1, x2)) = 1 + x2
POL(U23_ga(x1, x2)) = x2
POL(U4_GAGA(x1, x2, x3)) = x3
POL(halfcA_in_ga(x1)) = 1 + x1
POL(halfcA_out_ga(x1, x2)) = 1 + x2
POL(halfcB_out_ga(x1, x2)) = x2
POL(s(x1)) = 1 + x1
halfcA_in_ga(0) → halfcA_out_ga(0, 0)
halfcA_in_ga(s(0)) → halfcA_out_ga(s(0), 0)
halfcA_in_ga(s(s(X1))) → U22_ga(X1, halfcA_in_ga(X1))
U23_ga(X1, halfcA_out_ga(X1, X2)) → halfcB_out_ga(X1, s(X2))
U22_ga(X1, halfcA_out_ga(X1, X2)) → halfcA_out_ga(s(s(X1)), s(X2))
PC_IN_GAGA(X1, X3) → U4_GAGA(X1, X3, U23_ga(X1, halfcA_in_ga(X1)))
halfcA_in_ga(0) → halfcA_out_ga(0, 0)
halfcA_in_ga(s(0)) → halfcA_out_ga(s(0), 0)
halfcA_in_ga(s(s(X1))) → U22_ga(X1, halfcA_in_ga(X1))
U23_ga(X1, halfcA_out_ga(X1, X2)) → halfcB_out_ga(X1, s(X2))
U22_ga(X1, halfcA_out_ga(X1, X2)) → halfcA_out_ga(s(s(X1)), s(X2))
halfcA_in_ga(x0)
U22_ga(x0, x1)
U23_ga(x0, x1)